// -*- C++ -*-
#include <cstdarg>
#include <cassert>
#include <vector>
#include <set>
#include <sstream>
#include <stdint.h>
#include "../symbolics.h"

struct Element {
    virtual void _void() {};
};

struct Serialise : virtual Element {
    virtual int size() = 0;
    virtual void write( char *where ) = 0;
    virtual std::string print() { return std::string(); }
};

// A building element of a circuit that provides an output value.
template< typename T >
struct Value : virtual Serialise {
    virtual T get( int i = 0 ) = 0;
    virtual int size() { return sizeof( T ); }
    virtual void write( char *where ) {
        *(T *)where = get();
    }

    std::string print() {
        std::stringstream s;
        s << get();
        return s.str();
    }
  virtual int build( divine::Expr* e ) = 0;
};

//contains information about inports (their ranges)
//state will not contain inport values in the symbolic
struct SymContainer
{
  typedef std::pair< uint32_t, uint32_t > Range;
  std::vector< Range > table;
  std::vector< uint32_t > sizes;

  SymContainer() {}

  //inputs have a range
  //register the range, returns the name (id)
  template< typename T >
  uint32_t ackn( T first, T last ) {
    Range id;
    id.first = first;
    id.second = last + 1;
    table.push_back( id );
    return table.size() - 1;
  }

  //register delays and other store variables
  uint32_t ackn( uint32_t size ) {
    sizes.push_back( size );
    return sizes.size() - 1;
  }
};

struct Set {
  int maxVal;
  int sum;
  std::vector< uint32_t > *sizes, unfits;
  SymContainer *s;
  std::vector< std::vector< uint32_t > > unblobbed, partial, inputs;

  Set() {}
  
  void init( SymContainer *_s ) {
    s = _s;
    maxVal = 1;
    for ( int i = 0; i < s->table.size(); i++ ) {
      maxVal *= (s->table.at( i ).second - s->table.at( i ).first);
    }
    unblobbed.clear();
    partial.clear();
    inputs.clear();
    unfits.clear();
    
    sum = 0;
    std::vector< uint32_t > temp;
    sizes = &(s->sizes);
    for ( int i = 0; i < sizes->size(); i++ ) {
      sum += sizes->at( i );
      temp.push_back( 0 );
    }
    unblobbed.push_back( temp );
  }

  void addSeq( int max ) {
    std::vector< uint32_t > temp;
    temp.resize( s->table.size() + sizes->size() );
    for ( int i = 0; i < s->table.size(); i++ ) {
      temp.at( i ) = getInport( max, i );
    }
    for ( int i = 0; i < sizes->size(); i++ ) {
      temp.at( s->table.size() + i ) = getDelay( max, i );
    }
    partial.push_back( temp );
  }

  void accSeq( int index ) {
    partial.push_back( inputs.at( index ) );
  }

  void swap() {
    inputs = partial;
    partial.clear();
  }

  void generateInputs() {
    if ( inputs.size() == max() )
      return;
    inputs.clear();
    for ( int i = 0; i < max(); i++ )
      addSeq( i );
    swap();
  }

  uint32_t getDelay( int max, int index ) {
    return ((inputs.empty()) ?
            unblobbed.at( max / maxVal ).at( index ) :
            inputs.at( max ).at( s->table.size() + index ));
  }

  uint32_t getInport( int max, int index ) {
    if ( inputs.empty() ) {
      int m = max;
      for ( int j = 0; j < s->table.size(); j++ ) {
        if ( j == index ) {
          return s->table.at( j ).first +
            (m % (s->table.at( j ).second - s->table.at( j ).first));
        }
        m = m / (s->table.at( j ).second - s->table.at( j ).first);
      }
    }
    else
      return inputs.at( max ).at( index );
  }

  void prepTick() {
    std::vector< uint32_t > temp;
    temp.resize( sizes->size() );
    for ( int i = 0 ; i < inputs.size(); i++ ) {
      partial.push_back( temp );
    }
  }

  void read( uint32_t number, char *states ) {
    char *table = states;
    std::vector< uint32_t > temp;
    unblobbed.clear();
    uint32_t tempVar;
    for ( uint32_t i = 0; i < number; i++ ) {
      temp.clear();
      for ( int j = 0; j < sizes->size(); j++ ) {
        switch ( sizes->at( j ) ) {
        case 1:
          tempVar = *reinterpret_cast< uint8_t* >( table );
          break;
        case 2:
          tempVar = *reinterpret_cast< uint16_t* >( table );
          break;
        case 4:
          tempVar = *reinterpret_cast< uint32_t* >( table );
          break;
        }

        temp.push_back( tempVar );
        table += sizes->at( j );
      }
      unblobbed.push_back( temp );
    }
    partial.clear();
  }

  //we expect that blob has enough size
  void write( char *blob ) {
    char *table = blob;
    *reinterpret_cast< uint32_t* >( table ) = unblobbed.size();
    table += 4;
    for ( int i = 0; i < unblobbed.size(); i++ ) {
      for ( int j = 0; j < sizes->size(); j++ ) {
        *reinterpret_cast< uint32_t* >( table ) = unblobbed.at( i ).at( j );
        table += sizes->at( j );
      }
    }
  }

  int max() {
    return maxVal * unblobbed.size();
  }
  
  void prune() {
    //prune duplicite elements
    std::set< std::vector< uint32_t > > tempSet;
    for ( int i = 0; i < partial.size(); i++ ) {
      tempSet.insert( partial.at( i ) );
    }
    partial.clear();
    unblobbed.clear();
    inputs.clear();
    for ( std::set< std::vector< uint32_t > >::iterator it = tempSet.begin();
          it != tempSet.end(); it++ ) {
      unblobbed.push_back( *it );
    }
  }

  int size() {
    return sum * unblobbed.size() + 12;
  }

  std::string print( int i ) {
    std::stringstream s;
    s << "{";
    for ( int j = 0; j < unblobbed.at( i ).size(); j++ ) {
      s << unblobbed.at( i ).at( j );
      if ( j + 1 != unblobbed.at( i ).size() )
        s << ", ";
    }
    s << "}";
    return s.str();
  }
};

// An input *port*, for use within building blocks.
template< typename T >
struct In : Element {
    Value< T > *p;
    Value< T > *operator->() { return p; }
    In() { p = 0; }
};

struct Block : Element {
  SymContainer sc;
  Set _set;
  divine::SMTRep smt;
  
    typedef std::pair< Element *, Element * > Connection;
    std::vector< Connection > conns;

    // Connect a value-providing block to an input port.
    template< typename T >
    void connect( Value< T > &from, Element &parent, In< T > &to )
    {
        to.p = &from;
        conns.push_back( std::make_pair( &from, &parent ) );
    }

    // Connect a value-providing block to an input port.
    template< typename S, typename T >
    void connect( Value< S > &from, T &parent, int idx )
    {
        parent.in( idx ).p = &from;
        conns.push_back( std::make_pair( &from, &parent ) );
    }
};

template< typename T, int Max >
struct InSet {
    typedef std::vector< In< T > > Set;
    typedef typename Set::iterator iterator;
    Set set;

    In< T > &operator()( int idx ) {
	assert( idx < Max );
        if ( set.size() <= idx )
            set.resize( idx + 1 );
        return set[ idx ];
    }

    iterator begin() { return set.begin(); }
    iterator end() { return set.end(); }

  int size() { return set.size(); }

  In< T >& at( int i ) { return set.at( i ); }
};

// A building element of a circuit that needs to act upon the clock signal.
struct Clock {
    virtual void tick() = 0;
};

// A stateful building element: maintains (serialisable) state and reacts to
// clock ticks.
struct Stateful : virtual Clock, virtual Serialise {
  uint32_t name;
  SymContainer *tab;
  Set *symSet;

  Stateful(): name( 0 ), tab( 0 ), symSet( 0 ) {}

  void reg_symbolic( SymContainer *sc, Set *s ) {
    tab = sc;
    symSet = s;
  }

  virtual void reg_sizes() = 0;
  
    virtual void read( char *from ) = 0;
};

struct Referenceable : virtual Element {
  virtual void top( divine::SMTRep *, divine::Expr * ) = 0;
};

struct ArbSystem : Clock
{
  typedef std::vector< Stateful* > Elements;
  Elements elements;
  Block *_circuit;

  template< typename T >
  T *circuit() {
    return static_cast< T* >( _circuit );
  }


  ArbSystem() {}

  ArbSystem( Block &b ) {
    int swaps;

    /* TODO: There are probably better than cubic top-sort algorithms... */
    for ( int iter = 0; iter < b.conns.size(); ++iter ) {
      for ( int i = 0; i < b.conns.size(); ++i ) {
        for ( int j = 0; j < i; ++j ) {
          if (b.conns[j].first == b.conns[i].second &&
              b.conns[j].first != b.conns[j].second) {
            std::swap(b.conns[j], b.conns[i]);
            ++ swaps;
          }
        }
      }
    };

    for ( int i = 0; i < b.conns.size(); ++i ) {
      Stateful *s = dynamic_cast< Stateful * >( b.conns[i].first );
      if ( s )
        elements.push_back( s );
    }

    _circuit = &b;
  }

  virtual void tick() = 0;
  virtual int size() = 0;
  virtual void write( char * ) = 0;
  virtual void read( char * ) = 0;
  virtual std::string print() = 0;
};

struct SMTSystem: ArbSystem
{
  divine::SMTRep *_smt;
  
  SMTSystem( Block &b ): ArbSystem( b ) {
    _smt = &(_circuit->smt);
    for ( Elements::iterator i = elements.begin(); i != elements.end(); i++ ) {
      (*i)->reg_symbolic( &(_circuit->sc), &(_circuit->_set) );
      (*i)->reg_sizes();
    }
    _circuit->_set.init( &(_circuit->sc) );
    
    Referenceable *r;
    divine::Expr e;
    e.smt = _smt;
    std::set< Element* > tempS;
    for ( int i = 0; i < b.conns.size(); i++ ) {
      tempS.insert( b.conns.at( i ).first );
      tempS.insert( b.conns.at( i ).second );
    }

    for ( typename std::set< Element* >::iterator it = tempS.begin();
          it != tempS.end(); it++ ) {
      e.clear();
      r = 0;
      r = dynamic_cast< Referenceable* >( *it );
      if ( !r )
        continue;
      r->top( _smt, &e );
    }
  }

  void tick() {
    std::cout << "tick" << std::endl;//debug
    _smt->tick();
  }

  int size() {
    return _smt->size();
  }

  void read( char *c ) {
    _smt->read( c );
  }

  void write( char *c ) {
    _smt->write( c );
  }

  std::string print() {
    return _smt->print();
  }

  //new
  bool pc_sat( bool l ) {
    return _smt->pc_sat( l );
  }
};

struct SymSystem: ArbSystem
{
  SymSystem( Block &b ): ArbSystem( b ) {
    for ( Elements::iterator i = elements.begin(); i != elements.end(); i++ ) {
      (*i)->reg_symbolic( &(_circuit->sc), &(_circuit->_set) );
      (*i)->reg_sizes();
    }
    _circuit->_set.init( &(_circuit->sc) );
  }

  void tick() {
    for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i )
      (*i)->tick();
  }
  
  void prune() {
    _circuit->_set.prune();
  }

  int size() {
    return _circuit->_set.size();
  }

  void write( char *where ) {
    _circuit->_set.write( where );
  }

  void read( char *from ) {
    uint32_t number = *reinterpret_cast< uint32_t* >( from );
    _circuit->_set.read( number, from + 4 );
  }

  std::string print() {
    std::string s = "[";
    for ( int i = 0; i < _circuit->_set.unblobbed.size(); i++ ) {
      s += _circuit->_set.print( i );
    }
    s += "]";
    return s;
  }
};

// This class wraps the complete system and provides a single synchronised
// clock for all the stateful elements.
struct System : ArbSystem
{
  System( Block &b ): ArbSystem( b ) {}

  void tick() {
    for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i )
      (*i)->tick();
  }
  
    int size() {
        int s = 0;
        for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i )
            s += (*i)->size();
        return s;
    }

    void write( char *where ) {
        for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i ) {
            (*i)->write( where );
            where += (*i)->size();
        }
    }

    void read( char *from ) {
        for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i ) {
            (*i)->read( from );
            from += (*i)->size();
        }
    }

    std::string print() {
        std::string s = "[";
        for ( Elements::iterator i = elements.begin(); i != elements.end(); ++i ) {
            s += (*i)->print();
            if ( i + 1 != elements.end() )
                s += ", ";
        }
        s += "]";
        return s;
    }
};

// ------------ example block implementations -------------

namespace example {

// Implementation of the delay block. This is an example of a stateful element.
template< typename T >
struct Delay : virtual Value< T >, virtual Clock, virtual Stateful {
    In< T > in;
    T last;
    virtual T get() { return last; }
    void tick() { last = in->get(); }
    void read( char *from ) {
        last = *(T *)from;
    }
    Delay() : last() {}
};

// An input *block* (not a port).
template< typename T >
struct Input : virtual Value< T >, virtual In< T >, virtual Stateful {
    T value;
    virtual T get() { return value; }
    Input() : value() {}
    Input( T t ) : value( t ) {}
    Input< T > &operator=( T t ) { value = t; return *this; }
    void tick() {}
    void read( char *from ) {
        value = *(T *)from;
    }
};

// A simple output *block*.
template< typename T >
struct Output : Value< T > {
    Value< T > *from;
    virtual T get() { return from->get(); }
};

// A type-cast block.
template< typename From, typename To >
struct Cast : Value< To > {
    In< From > in;

    virtual To get() {
        return static_cast< To >( in->get() );
    }
};

template< typename T >
struct Sum : Value< T > {
    InSet< T, 4 > in;

    virtual T get() {
        T acc = 0;
        for ( typename InSet< T, 4 >::iterator i = in.begin(); i != in.end(); ++i )
            acc += (*i)->get();
        return acc;
    }
};

template< typename T >
struct Product : Value< T > {
    In< T > a, b;

    virtual T get() {
        return a->get() * b->get();
    }
};

template< typename T >
struct Min : Value< T > {
    In< T > a, b;

    virtual T get() {
        return std::min( a->get(), b->get() );
    }
};

template< typename T >
struct Gain : Value< T > {
    In< T > in;
    T value;

    virtual T get() {
        return value * in->get();
    }

    Gain( T v ) : value( v ) {}
};

template< typename T >
struct MinMax : Value< T > {
    In< T > a, b;
    enum Function { Min, Max };
    Function f;

    MinMax( Function _f ) : f( _f ) {}
    T get() {
        switch (f) {
            case Min: return std::min( a->get(), b->get() );
            case Max: return std::max( a->get(), b->get() );
        }
    }
};

}
